T:Type, L:(T List), R:({x:T| (x  L)} Realizer).
(T r Id)
 (xL. R-Feasible(R(x)))
 (xL. i:Id. R-has-loc(R(x);i) = x = i  )
 (xL. yL. R-icompat(R(x);R(y)))
 R-Feasible(xL.R(x)) 

latex

Definitions	P  Q, True, T, P  Q, P & Q, A, SQType(T), {T}, , x. t(x), t  T, P  Q, x(s), xL. P(x), P  Q, x:A. B(x), False, Dec(P)
Lemmas	assert-eq-id, true wf, squash wf, assert wf, es realizer wf, R-Feasible wf, eq id wf, R-has-loc wf, bool wf, Id wf, R-icompat wf, l all wf2, R-compat-disjoint, R-compat wf, Id sq, decidable equal Id, l member wf, R-feasible-Rall